Nuprl Lemma : R-possible_wf
0,22
postcript
pdf
R
:es_realizer{i:l},
es
:ES{i}. R-possible{i:l}(
R
;
es
)
Prop{i'}
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
Prop
,
Possible(
R
;
es
)
,
A
&
B
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
P
Q
Lemmas
R-Feasible
wf
,
world
wf
,
fair-fifo
wf
,
possible-world
wf
,
R-Dsys
wf
,
event
system
wf
,
w-es
wf
,
es
realizer
wf
origin
R:es_realizer{i:l}, es:ES{i}. R-possible{i:l}(R; es) 
Prop{i'} R:es_realizer{i:l}, es:ES{i}. R-possible{i:l}(R; es) Prop{i'} x:A. B(x) T
x:A. B(x)
Q